#include "dimac_parser.h"
#include<string.h>
#include<stdlib.h>
dimac_parser* parser_init(const char* fn){
    dimac_parser* parser = (dimac_parser*)malloc(sizeof(dimac_parser));
    strncpy(parser->filename, fn, 128);
    if((parser->fp = fopen(parser->filename, "r")) == NULL){
        printf("error while opening file %s\n", parser->filename);
        free(parser);
        return NULL;
    }
    return parser;
}
static variable temp_vars[1000];
int parse(dimac_parser* parser, cnf* cnf){
    if (cnf == NULL || parser == NULL){
        printf("parser or cnf isn't inited\n");
        return -1;
    }
    if (parser->fp == NULL){
        printf("parser not inited\n");
        return -1;
    }
    _bool formulastart = false;
    int nclause = -1, nvar = -1, cls_count = 0;
    while(EOF != fscanf(parser->fp, "%[^\n]%*c", parser->buf)){
        //printf("fs: %s\n", parser->buf);  
        //break;
        int length = strlen(parser->buf);
        char* pt = &parser->buf[0];
        _bool comment = false;
        _bool declare = false;
        _bool err = false;
        for(int i = 0; (!formulastart && !comment) && i < length; i++, pt++){
            switch (*pt){
                case 'c':
                    //printf("comment: %s\n", parser->buf);
                    comment = true;
                    break;
                case 'p':
                    printf("start of formula\n");
                    formulastart = declare = true;
                    break;
                default:
                    if (!formulastart)
                        err = true;
                    break;
            }    
            if (err){
                printf("parse error: %s\n", parser->buf);
                return -1;
            }     
        }  
        if (comment){
            continue;
        }
        if (formulastart){
            if(declare){
                int length = strlen(parser->buf);
                pt = &parser->buf[0];
                for(int i=0; i < length-3; i++, pt++){
                    if(*pt == 'c' && *(pt+1) == 'n' && *(pt+2) == 'f'){
                        break;
                    }
                }
                pt = pt+3;
                if(EOF != sscanf(pt, " %d %d", &nvar, &nclause)){
                    printf("formula has %d vars and %d clause\n", nvar, nclause);
                }
                declare = false;
                assert(nclause > 0 && nvar > 0);
            }
            else{
                //printf("new clause\n");
                int readnum = 0, readlen = 0;
                char* pt = &parser->buf[0];
                clause* cls = (clause*)malloc(sizeof(clause));
                cls->vars = &temp_vars[0];
                cls->true_val = cls->true_val_available = false;
                cls->var_num = 0;
                while(1){
                    readlen = sscanf(pt, "%d", &readnum);
                    if (readnum == 0 || readlen == 0) {
                        if (pt[0] == '%'){
                            //printf("%s ???\n", pt);
                            free(cls);
                            return 0;
                        }
                        break;
                    }
                    else{
                        int n, num;
                        n = readnum > 0 ? 1 : 2;
                        num = readnum > 0 ? readnum: -readnum;
                        while(num){
                            num /= 10;
                            n++;
                        }
                        pt += n;
                        //printf("pt: %s\n", pt);
                        //printf("new num %d, \n", readnum);
                        cls->vars[cls->var_num].flag = 0;
                        cls->vars[cls->var_num].sign = readnum > 0 ? 1 : 0;
                        cls->vars[cls->var_num++].name = readnum > 0 ? readnum : -readnum; 
                        //printf("new num %d, sign%d\n", readnum, cls->vars[cls->var_num-1].flag);
                    }
                }
                add_clause(cnf, cls);
                free(cls);
            }    
        }
    }
    return -1;
}